Nuprl Lemma : count_wf
4,23
postcript
pdf
A
:Type,
P
:(
A
),
L
:
A
List. count(
P
;
L
)
latex
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
count(
P
;
L
)
,
A
B
,
P
Q
,
False
,
A
,
,
if
b
t
else
f
fi
,
True
,
T
Lemmas
reduce
wf
,
nat
wf
,
ifthenelse
wf
,
le
wf
,
bool
wf
origin
A:Type, P:(A
), L:A List. count(P;L) 
A:Type, P:(A), L:A List. count(P;L) Tx:A. B(x)
B
Q
A
t else f fi
T